$\forall$$T$:Type, ${\it sz}$:$\mathbb{N}^{+}$, ${\it eq}$:($T$$\rightarrow$$T$$\rightarrow\mathbb{B}$), $f$:($\mathbb{N}\rightarrow$$T$). random{-}seq($T$;${\it sz}$;${\it eq}$;$f$) $\in$ Prop